Skip to content

Fix bool versus bitvec 1 sort mismtach for CVC4 #6205

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 1 commit into from
Jul 6, 2021
Merged

Fix bool versus bitvec 1 sort mismtach for CVC4 #6205

merged 1 commit into from
Jul 6, 2021

Conversation

TGWDB
Copy link
Contributor

@TGWDB TGWDB commented Jun 28, 2021 •
edited
Loading

This fixes a sort mismatch that can occur in CVC4 where an
array of booleans is translated into an array of (_ bitvec 1)
which is then a mismatch when CVC4 expects and can handle an
Array of Bool.

This solves some of the problems in #5977 .

Note that there are NO TESTS for this since we do not support cvc4 in CI.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@TGWDB
Fix bool versus bitvec 1 sort mismtach for CVC4
081649e 
This fixes a sort mismatch that can occur in CVC4 where an
array of booleans is translated into an array of (_ bitvec 1)
which is then a mismatch when CVC4 expects and can handle an
Array of Bool.
@kroening
Copy link
Member

All relevant solvers support arrays of bool now -- I'll do a PR that removes the (_ bitvec 1) encoding.

@codecov
Copy link

codecov bot commented Jun 28, 2021

Codecov Report

Merging #6205 (081649e) into develop (0002950) will increase coverage by 7.55%.
The diff coverage is n/a.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #6205      +/-   ##
===========================================
+ Coverage    67.40%   74.95%   +7.55%     
===========================================
  Files         1157     1456     +299     
  Lines        95236   161192   +65956     
===========================================
+ Hits         64197   120829   +56632     
- Misses       31039    40363    +9324
Flag Coverage Δ
cproversmt2 ?
regression ?
unit ?

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files Coverage Δ
src/util/string_container.cpp 52.94% <0.00%> (-47.06%) ⬇️
src/solvers/prop/prop.cpp 42.85% <0.00%> (-41.76%) ⬇️
src/solvers/flattening/boolbv_member.cpp 53.65% <0.00%> (-38.65%) ⬇️
src/cpp/cpp_storage_spec.cpp 65.00% <0.00%> (-35.00%) ⬇️
src/util/cmdline.h 66.66% <0.00%> (-33.34%) ⬇️
src/solvers/strings/array_pool.h 66.66% <0.00%> (-33.34%) ⬇️
src/solvers/strings/string_refinement.h 66.66% <0.00%> (-33.34%) ⬇️
...rs/strings/string_concatenation_builtin_function.h 0.00% <0.00%> (-33.34%) ⬇️
src/cbmc/c_test_input_generator.cpp 60.00% <0.00%> (-30.33%) ⬇️
src/ansi-c/c_typecheck_base.cpp 54.39% <0.00%> (-26.51%) ⬇️
... and 1435 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 06c2cfd...081649e. Read the comment docs.

martin-cs
martin-cs requested changes Jun 29, 2021
View reviewed changes
Copy link
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This seems like a work-around rather than a fix. If you can find the code that is generating the sort mismatch then you should be able to fix this properly.

@TGWDB
Copy link
Contributor Author

TGWDB commented Jul 5, 2021

@kroening @martin-cs It would be nice to approve and merge this PR to allow cvc4 to not error, regardless of future fixes to resolve the sort stuff generally as in #6206 .

peterschrammel
peterschrammel approved these changes Jul 6, 2021
View reviewed changes
Copy link
Member

@peterschrammel peterschrammel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let's merge this workaround, with a proper fix expected in #6206.

martin-cs
martin-cs reviewed Jul 6, 2021
View reviewed changes
Copy link
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think this is a good idea as it is a work around. I am not sure #6206 will fix it either as I think that is needed for MathSAT support but ... @TGWDB if you really want to do it, I won't stand in your way.

martin-cs
martin-cs approved these changes Jul 6, 2021
View reviewed changes
Copy link
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't approve but this will remove my "request changes".

@TGWDB TGWDB merged commit 54c385e into diffblue:develop Jul 6, 2021
@TGWDB
Copy link
Contributor Author

TGWDB commented Jul 6, 2021

@martin-cs Thanks. This is kind of a blocking concern for AWS since it prevents many things that should work with cvc4 from progressing. I agree a proper look at the SMT2 back end and fixing details there is preferable, but this is likely to be slow and/or caught up with other changes. Let's hope a proper solution is done in future.

@TGWDB TGWDB mentioned this pull request Jul 12, 2021
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@peterschrammel peterschrammel peterschrammel approved these changes

@martin-cs martin-cs martin-cs approved these changes

@allredj allredj Awaiting requested review from allredj

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@romainbrenguier romainbrenguier Awaiting requested review from romainbrenguier

@tautschnig tautschnig Awaiting requested review from tautschnig

Assignees
No one assigned
Labels
SMT Backend Interface
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@TGWDB @kroening @peterschrammel @martin-cs